Nuprl Lemma : fpf-empty-sub
0,22
postcript
pdf
A
:Type,
B
,
eq
,
g
:Top.
g
latex
Definitions
t
T
,
False
,
P
Q
,
x
:
A
.
B
(
x
)
,
b
,
x
dom(
f
)
,
f
g
,
,
Top
Lemmas
top
wf
,
false
wf
origin
A:Type, B, eq, g:Top. 
g A:Type, B, eq, g:Top. g 
T
Qx:A. B(x)
b dom(f) g